$\forall$$L$:MsgA List. ma{-}is{-}empty($\oplus$($L$)) $\sim$ reduce($\lambda$$M$,$x$. ma{-}is{-}empty($M$) $\wedge_{2}$ $x$;true$_{2}$;$L$)